Adds a Hoare-style loop invariant rule for loopTM that enables
compositional reasoning about loops via a decreasing variant.

- complementTM_hoareTime: lifts original TM Hoare triple through
  complement, flipping output cell 1. Fully compositional.
- ifTM_hoareTime: composes test Hoare triple with branch completion.
  The user proves branching via existing per-phase simulation lemmas.
- Make compCfg, complementTM_simulation, complementTM_rewind_and_flip
  public for use in Hoare composition.

Extend ifTM_hoareTime to compose test, then-branch, and else-branch
Hoare triples without the user ever seeing reachesIn. The theorem
handles all internal phases (transition, rewind, check, branch routing)
automatically.

New infrastructure in IfInternal.lean:
- tape_writeAndMove_stable, tape_move_idleDir_stable: one-step identity
  for stable tapes during readBackWrite/idleDir phases
- ifTransitionTape_cells, ifTransitionInput_cells: cells preservation
- ifTransitionTape_head_ge, ifTransitionInput_head_ge: head bounds
- ifTM_rewind_loop_full: extended rewind tracking all tapes
- ifTM_check_step_then_full, ifTM_check_step_else_full: check steps
  tracking all tapes

…frastructure

Add Combinators/Internal/Generic.lean with shared proof tools:
- simulation_reachesIn: generic simulation lifting (wrap commutes with step)
- generic_rewind_loop / generic_rewind_loop_full: generic output-tape rewind
- Shared tape stability lemmas (deduplicated from 4 Internal files)

Restructure Combinators/Internal.lean into Internal/Union.lean (original
content, byte-identical) + Internal/Generic.lean, with Internal.lean as
aggregation.

Refactor all combinator Internal files to use the generic tools:
- 8 simulation proofs replaced with one-liner simulation_reachesIn calls
- 3 rewind loop proofs (complement, if, loop) delegate to generic_rewind_loop
- ~15 duplicated private tape lemmas removed

Add AllTapesWF.ifTransition and ifTransitionTape_head_bound helpers to
Hoare.lean, simplifying ifTM_hoareTime tape invariant threading.

All public theorem signatures preserved; only proof bodies changed.

Add the full UTM sub-machine scaffolding and prove the hardest piece
of readCurrentTM: the scan induction over super-cells with modular
arithmetic for the position counter.

Proved:
- copyState_simulation: Phase 1 copy loop (induction on k)
- scan base + inductive case: Phase 2 sim tape scanning
- readHi single-step: transition after marker found
- rewindSim_simulation: sim tape rewind (new theorem)
- rewindState_simulation, rewindScratch_simulation: Phase 3 rewinds
- checkHaltTM_hoareTime: full CheckHalt composition (1767 lines)
- per_tape_simulation composition skeleton

New files: ReadCurrent, ReadCurrentInternal, CheckHalt, CheckHaltInternal,
SimConfig/Defs, Init, Lookup, ApplyTransition, ExtractOutput, UTM.

12 sorry's remain across 6 UTM files (down from ~20+ at session start).

Add InitInternal module with sub-machines for UTM initialization:
Copy, Rewind, SetupState, SetupSim. Fix all non-sorry lint warnings
in CheckHaltInternal and ReadCurrentInternal (unused variables, unused
simp args, redundant intro).

Add tape helper lemmas (idle_tape_preserved, writeAndMove_*, etc.).
Fix theorem signatures: add desc/state head hypotheses, scratch head = n+1.
Partial phase1_loop proof: base case complete, inductive case needs hreach3.

Fill in the 3-step reachesIn proof (hreach3) completing the phase1_loop
theorem. Uses writeAndMove_cells_at_head/ne for sim tape cell tracking
and readBackWrite_cells for scratch tape preservation.

Extend phase1_loop postconditions with scratch cell preservation.
Prove setupSim_phase12 by composing phase1_loop (3n+1 steps) with
6 simWriteRight extras and 1 advanceInput step (3n+8 total).

Revert broken phase12 merge. Clean state: phase1_loop fully proved,
3 sorry's remaining (phase12, phase3, hoareTime).

Compose phase1_loop(done=0) with 6 simWriteRight extras and 1 advanceInput
step. Generic simwr_step helper handles all 6 extra steps uniformly.
Extended phase1_loop postconditions with scratch cell preservation.
Verified: lake env lean produces only sorry warnings for phase3/hoareTime.

- Complete proof of rewindScratch_loop (induction on scratch head h,
  h+1 steps from .rewindScratch to .bounceScratch with head 1)
- Stub stride_loop helper (sorry'd body)
- setupSim_phase3: suffices skeleton with generalized induction on
  remaining bits (processed counter), nil/cons cases sorry'd
- setupSimTM_hoareTime still sorry'd
- Other UTM files: upstream changes from prior sessions

…ear sim_head/ones/rest

…main

…_hoareTime remain

…nitEnvelope + head bounds)

…_hoareTime' has unprovable bound (B universally quantified)

UTM sorry elimination

…me' sig

- Add `rewindWorkTM_rich_hoareTime` to HelpersInternal.lean as public
  shared infrastructure. This preserves an arbitrary predicate P through
  rewindWorkTM, enabling data threading (descOnTape, stateOnTapeAt,
  superCellsCorrect) through rewind steps in seqTM compositions.
- Add `tape_idle_preserve` to HelpersInternal.lean (public).
- Remove duplicate private copies from CheckHaltInternal.lean.
- Fix `readCurrentTM_hoareTime'` signature: change universally quantified
  `B : ℕ` (unprovable for small B) to existential `∃ B`.
- Add `all_tapes_simulation` stub and helpers for Phase 2 iteration.

Close the Phase 2 iteration sorry: `all_tapes_simulation` iterates
`per_tape_simulation` over all n+2 simulated tapes by induction on
remaining tapes. `extract_sim_conditions` extracts per-tape marker/hi/lo
conditions from `superCellsCorrect` via case analysis on the tape index
(input/work/output).

Remaining sorry in ReadCurrentInternal: `readCurrentTM_hoareTime'` (main
composition of all 4 phases).

…lpers

- Prove `extract_sim_conditions`: extracts per-tape marker/hi/lo
  conditions from superCellsCorrect for any target tape index.
- Prove `all_tapes_simulation`: iterates per_tape_simulation over all
  n+2 tapes by induction, composing via reachesIn_trans.
- Add simHeadPos, simCellsFn helpers for tape iteration.
- readCurrentTM_hoareTime' still sorry'd (composition + scratchHasInputPattern).

…e sig

Build the seqTM_hoareTime composition infrastructure for initTM_hoareTime':
- Define copyData and setupStateData predicates for data-preserving rewinds
- Prove preservation lemmas: copyData_preserved, setupStateData_preserved
- Prove bridge lemmas: postCopy_to_copyData, postCopy_to_rewind0Pre,
  setupStatePost_to_rewind3Pre, postSetupSim_to_rewindAll (with initData)
- Sketch main composition via 5 nested seqTM_hoareTime calls
- Fix initTM_hoareTime signature: universal B→∃B, add full precondition

Remaining sorry's in InitInternal.lean: rewind0/3 HoareTime specs,
copyDataHead1/setupStateDataHead1 bridge lemmas, main composition.

…served

Fully prove:
- setupStateData_preserved: data survives rewind of tape 3
- rewind3_setupStateData_hoareTime: rich rewind for phase 4

Remaining sorry's: rewind0 pre-adaptation (read conditions),
copyDataHead1/setupStateDataHead1 bridges, main composition.

Fully prove:
- copyDataHead1_to_setupStatePre: InitEnvelope + setupState pre from copyData
- rewind3_setupStateData_hoareTime: rich rewind for phase 4
- setupStateData_preserved: data survives tape 3 rewind
- h_copyData_env partially addressed (head ≥ 1 added to copyData)

Remaining sorry's in InitInternal: rewind0 read conditions (4 sub-goals),
setupStateDataHead1_to_setupSimPre, h_copyData_env.

…etupStatePre

Close 4 more sorry's in InitInternal.lean:
- rewind0_copyData_hoareTime: rich rewind for phase 2 (tape 0), including
  initTape cell analysis for read conditions
- copyDataHead1_to_setupStatePre: fully proved with InitEnvelope reconstruction
- h_copyData_env: uses copyDataHead1_to_setupStatePre bridge

Remaining sorry's in InitInternal.lean: setupStateDataHead1_to_setupSimPre
(inp layout bridge) and h_copyData_env (InitEnvelope from copyData).

…analysis

Close the rewind0 sorry including all 4 read-condition sub-goals:
- inp.read ≠ Γ.start via initTape + encodeUTMInput_ne_start
- out.read ≠ Γ.start via initTape [] at position 1
- Work tape reads via initTape [] at position 1
- Bound omega

Remaining: 2 sorry's in InitInternal (h_copyData_env, setupStateDataHead1).

…ucture

Major progress on initTM_hoareTime' composition:
- Extract shared initTape_cells_ne_start and copyData_to_initEnvelope helpers
- Fully prove h_copyData_env (InitEnvelope from copyData)
- Prove setupStateDataHead1_to_setupSimPre structure with sorry's
  for fields not in setupState postcondition
- Strengthen setupStateData with sim head, state head bound, inp layout
- Fix setupStateData_preserved for new fields

Remaining sorry's are well-localized:
- setupStatePost_to_rewind3Pre: 4 sorry's (sim head=1, state head≤k+1,
  inp.cells, inp.head) — need setupStateTM_hoareTime postcondition
  strengthening (setupState preserves sim/inp, bounds state head)
- setupStateDataHead1_to_setupSimPre: 3 sorry's (encodeUTMInput
  structure at specific positions — separator, x data, sentinel)

Close 4 more sorry's:
- setupStateTM_simulation/hoareTime: add state head = k+1 / ≤ k+1 to
  postcondition (trivially from existing hst_h4 in phase4 claim)
- setupStateDataHead1_to_setupSimPre: prove all 3 encodeUTMInput layout
  facts (separator, x data, end sentinel) via List.getElem?_append_right
  + List.getElem?_cons_succ

Remaining: 3 sorry's in setupStatePost_to_rewind3Pre for sim head/inp
preservation through setupState (need step-level idle tape preservation).

Major milestone: initTM_hoareTime' composition is fully proved (modulo
upstream sorry's in SetupState/SetupSim sub-machine proofs).

Changes to SetupState.lean:
- Add state head ≤ k+1, sim tape preservation, input preservation to
  setupStateTM_simulation and setupStateTM_hoareTime postconditions
- sim/input preservation sorry'd (need step-level idle tape analysis:
  setupState writes blank to blank sim cells with stay direction = identity,
  and input tape only moves with idleDir = stay when read ≠ ▷)

Changes to InitInternal.lean:
- Close all 7 sorry's: encodeUTMInput layout facts, InitEnvelope
  reconstruction, h_copyData_env bridge, setupStatePost bridge,
  setupStateDataHead1 bridge
- Full composition structure proven via 5 nested seqTM_hoareTime calls
  with rich rewind specs and data-preserving predicates

Prove that setupStateTM preserves sim tape (tape 2) and input tape
through any execution:

- idle_tape_initTape: writeAndMove blank/stay on blank cell = identity
- idle_input: move stay on input = identity
- setupStateTM_sim_tape_idle: transition writes blank with idleDir to sim
- setupStateTM_inp_dir_idle: transition uses idleDir for input direction
- setupStateTM_step_sim_preserved: one step preserves sim tape
- setupStateTM_step_inp_preserved: one step preserves input tape
- setupStateTM_reachesIn_sim_preserved: full execution preserves sim
- setupStateTM_reachesIn_inp_preserved: full execution preserves input

Both InitInternal.lean and SetupState.lean now have ZERO sorry's.
The initTM_hoareTime' composition proof is complete.

…nd sub-machine definitions

- Strengthen all_tapes_simulation with hsc_vals₂ conjunct exposing per-cell
  encoded symbol values written to scratch tape for each simulated tape
- Add hsc_above conjunct to per_tape_simulation for cells above written range
- Add reachesIn_toReaches' helper for reachesIn → reaches conversion
- Compose readCurrentTM_hoareTime' proof structure with all 4 phases
  (copyState → all_tapes → rewindState → rewindScratch); 3 sorry's remain:
  bound B value, t ≤ B, and scratchHasInputPattern postcondition
- Expand lookupTM/applyTransitionTM definitions with proper state machines
- Extract initTM definition to Init/Defs.lean to break circular import
- Add extractOutputTM proper definition with rewind + scan + decode

…lyTransition

Close all 4 ExtractOutput sorry's:
- sim_cells_ne_start_of_scc: super-cell cells ≥ 1 are never ▷
- rewind_output_phase: output tape rewind by induction on head position
- scanSim_phase: sim tape scan by induction on remaining count
- extractOutputTM_hoareTime: 6-phase composition (rewind → rightOut →
  scanSim → readHi → readLo → writeOut → done)

Added inp.read ≠ Γ.start to extractOutputTM_hoareTime precondition
(valid in UTM context where input has been processed).

Expand Lookup/ApplyTransition Fintype instances and δ_right_of_start
(fully proved, no sorry's). Lookup/ApplyTransition HoareTime proofs
remain sorry'd (Tier B).

4 sorry's remain: lookupTM_hoareTime, applyTransitionTM_hoareTime,
utm_simulates, utm_correct.

Replace all `.blank` work writes with `readBackWrite (wHeads i)` and
`.blank` output writes with `readBackWrite oHead` for non-halt state
transitions. The previous `allIdle`-based transitions wrote `Γ.blank`
at all tape head positions, corrupting data on desc/scratch/state/sim
tapes.

Also fix matchRewindR to advance desc past the separator bit (Dir3.right
for utmDescTape), so copyOutput starts reading from the first output bit
rather than the separator.

Strengthen lookupTM_hoareTime precondition with `desc = encodeTM tm`,
per-tape head bounds, and input/output tape conditions.

Create LookupInternal.lean with:
- Tape helper lemmas (readBackWrite, idle preserve, write_head)
- Encoding lemmas (input pattern, trans output, entry lengths)
- skipHeader_loop — fully proved (induction on remaining header bits)
- skipRest_loop — fully proved (induction on remaining entry bits)
- rewindScratchFinal_loop — fully proved (induction on head position)
- Phase simulation stubs for: compare_match_loop, compare_mismatch,
  rewindScratch_loop, process_nonmatch_entry, entry_scan_to_match,
  matchRewind_loop, matchRewindR_step, copyOutput_loop, rewindDesc_loop
- lookupTimeBound time bound definition

Close rewindScratch_loop, matchRewind_loop, rewindDesc_loop,
rewindScratchFinal_loop, matchRewindR_step, and skipRest_loop.

Remaining sorry's: compare_match_loop, compare_mismatch,
process_nonmatch_entry, entry_scan_to_match, copyOutput_loop.

…condition

5 sorry's remain: compare_match_loop, compare_mismatch,
process_nonmatch_entry, entry_scan_to_match, copyOutput_loop.

Key blocker: dite reduction in compare state δ transition.

Use split_ifs to handle nested if/dite in compare state transitions.
This resolves the core blocker for compare_match_loop proof.

Close all sorry's except copyOutput_loop. Proved:
- compare_match_loop via generalized induction on ipw-pos
- compare_mismatch via generalized induction on mismatchPos
- process_nonmatch_entry via composition
- entry_scan_to_match via induction on numBefore

Key technique: split_ifs handles nested if/dite in compare δ.
Used simp [Nat.add_assoc] to fix Fin equality with dependent proofs.

Complete phase decomposition proofs for lookupTM:
- skipHeader_loop: skip header bits on desc tape
- compare_match_loop: compare all ipw bits, full match
- compare_mismatch: compare with mismatch at given position
- skipRest_loop: skip remaining entry bits after mismatch
- rewindScratch_loop: rewind scratch after mismatch
- process_nonmatch_entry: compose mismatch phases
- entry_scan_to_match: scan past non-matching entries
- matchRewind_loop: rewind scratch after match
- matchRewindR_step: advance desc past separator
- copyOutput_loop: copy output bits from desc to scratch
- rewindDesc_loop: rewind desc to cell 1
- rewindScratchFinal_loop: final scratch rewind and halt

Key techniques:
- split_ifs for nested if/dite in compare transitions
- suffices with generalized induction for compare/mismatch loops
- Function.update reasoning for copyOutput cell tracking

…sorry's

Add lookupTM_hoareTime_proof in LookupInternal.lean with the full
phase composition structure. The proof chains all 12 phase lemmas
via reachesIn_trans and verifies the postcondition.

7 sorry's remain, all in encoding-level facts:
- Transition table structure from desc = encodeTM tm
- Entry matching/non-matching conditions
- Time bound calculation
- Output bits correctness

The phase simulation proofs (2034 lines) are complete.
The encoding connection is the remaining work.

…dition

- Extend copyOutput_loop postcondition with desc cells preservation,
  scratch head position (= ow + 1), and scratch cells beyond ow preserved
- Close scratch head sorry: (c₅.work utmScratchTape).head ≥ 1
- Close desc cells sorry: chain cells preservation through all 7 phases
- Close blank sentinel sorry: trace cell ow+1 back through phases
- Add encoding helpers: allΓ_complete, allΓFuncs_complete, Γ_ofBool_injective
- Add preconditions: desc head = 1, scratch sentinel cell = blank
- Update Lookup.lean public spec to match

Remaining sorry's: encoding connection (henc_connection) and time bound.

- Add encodeTransTable_eq_allTuples_flatMap: connects transTable to allTuples.flatMap
- Add allTuples_entryFn and allTuples_entryFn_width: entry function with constant width
- Close matching entry (refine_2): chain desc tape → table bits → entry bits → scratch
- Close output bits (refine_3): same chain with encodeEntry_output_getElem
- Remaining: non-matching entries (needs allTuples_nodup) and time bound

- Add allΓ_nodup: allΓ has no duplicates (by decide)
- Add allTuples_nodup scaffold: levels 1-2 proved (pairwise disjoint by
  tuple component), level 3 needs allΓFuncs_nodup (sorry)
- Clean up non-matching entries proof to document approach
- 3 sorry's remain in LookupInternal: allΓFuncs_nodup (in allTuples_nodup),
  non-matching entries (blocked on nodup), time bound

…TComputable)

Add foundational infrastructure for cryptographic formalization:

- BitEncodable: specification-level typeclass for encoding types as
  bit strings, with instances for Unit, List Bool, Option, and Prod.
- unpair: left inverse of pair, with roundtrip proof.
- PPTComputable: predicate asserting a randomized function
  (List Bool → PMF (List Bool)) is computable by a PPT NTM, bridging
  NTM output distributions to Mathlib's PMF via ENNReal.
- Make pair_nil_eq and pair_cons_eq public @[simp] lemmas.